the_es:ES. Trans x,y:E. x c y 

latex

Definitions	e c e', Trans x,y:T. E(x;y), P  Q, P  Q, (e < e'), Prop, E, ES, x:A. B(x), t  T, P & Q, {T}
Lemmas	es-axioms, event system wf, es-E wf, es-causl wf